Nuprl Lemma : comb_for_rng_when_wf
6,26
postcript
pdf
(
r
,
b
,
p
,
z
. when
b
.
p
)
r
:Rng
|
r
|
True
|
r
|
latex
Definitions
t
T
,
Rng
,
T
,
x
:
A
.
B
(
x
)
,
Prop
Lemmas
rng
when
wf
,
squash
wf
,
true
wf
,
rng
car
wf
,
bool
wf
,
rng
wf
origin
r,b,p,z. when b. p) 
r:Rng
|r|
True|r| r,b,p,z. when b. p) r:Rng|r|True|r| TT
x:A. B(x)